Code(/home/psksvp/workspace/sv-bench/c/loop-acceleration/diamond_true-unreach-call2.c,false,clang-3.7,200)

extern void __VERIFIER_error() __attribute__ ((__noreturn__));
extern unsigned int __VERIFIER_nondet_uint(void);

void __VERIFIER_assert(int cond) {
  if (!(cond)) {
    ERROR: __VERIFIER_error();
  }
  return;
}

int main(void) {
  unsigned int x = 0;
  unsigned int y = __VERIFIER_nondet_uint();

  while (x < 99) {
    if (y % 2 == 0) x += 2;
    else x++;

    if (y % 2 == 0) x += 2;
    else x -= 2;

    if (y % 2 == 0) x += 2;
    else x += 2;

    if (y % 2 == 0) x += 2;
    else x -= 2;

    if (y % 2 == 0) x += 2;
    else x += 2;

    if (y % 2 == 0) x += 2;
    else x -= 4;

    if (y % 2 == 0) x += 2;
    else x += 4;

    if (y % 2 == 0) x += 2;
    else x += 2;

    if (y % 2 == 0) x += 2;
    else x -= 4;

    if (y % 2 == 0) x += 2;
    else x -= 4;
  }

  //__VERIFIER_assert((x % 2) == (y % 2));
  if(!((x % 2) == (y % 2))) __VERIFIER_error();
}

define i32 @main() #0  { 
  
    %1 = alloca i32, align 4
    %x = alloca i32, align 4
    %y = alloca i32, align 4
    store i32 0, i32* %1
    store i32 0, i32* %x, align 4, !dbg !17
    %2 = call i32 @__VERIFIER_nondet_uint() , !dbg !18
    store i32 %2, i32* %y, align 4, !dbg !19
    br label %3, !dbg !20
  
  ;